A:Type, eq:EqDecider(A), B:(AType), f:fpf(A; a.B(a)), x:A, v:B(x).
fpf-compatible(A; a.B(a); eq; f; fpf-single(x; v))
 (fpf-dom(eq; x; f))
 (fpf-ap(f; eq; x) = v) 

latex

Definitions	t  T, top, P  Q, P  Q, x:A. B(x), P  Q, P  Q, x(s), fpf-ap(f; eq; x), b, fpf-compatible(A; a.B(a); eq; f; g), EqDecider(T), x. t(x), fpf(A; a.B(a)), fpf-single(x; v), fpf-dom(eq; x; f)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-compatible wf, fpf-single wf, fpf wf, deq wf, fpf-single-dom